R:Realizer. R-Feasible(R)  ([[R]]  Dsys) 

latex

Definitions

True, T, ff, P  Q, P  Q, tt, if b then t else f fi , Top, P & Q, , False, A, R-size(R), A  B, x. t(x), t  T, P  Q, x:A. B(x), , A c B, x(s), , Unit, Realizer, Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), S  T, left  right, Rnone(),

Lemmas

es realizer wf, Rrframe wf, Rbframe wf, Raframe wf, Rpre wf, Rsends wf, Reffect wf, Rsframe wf, Rframe wf, Rinit wf, Rplus wf, assert of lt int, bnot of le int, true wf, squash wf, eqff to assert, bnot wf, lt int wf, assert of le int, eqtt to assert, le wf, assert wf, iff transitivity, nat plus inc, nat wf, nat plus wf, R-size wf, le int wf, ifthenelse wf, R-compat-Dsys, m-sys-join wf2, R-Dsys-Rplus, R-Feasible-Rplus, Rnone wf, R-Feasible wf, R-Dsys-base-wf, bool wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, Id wf, unit wf